open import Relation.Unary using ( Pred ; U; Decidable )
open import Algebra.Structures using (  IsGroup ; IsAbelianGroup ; IsSemigroup)
open import Algebra using ( Group ; Monoid ; Semigroup ; AbelianGroup)
open import Relation.Binary using ( Rel )
open import Algebra.FunctionProperties using ( Op₁ ; Op₂ )
open import Level using ( Level ; _⊔_ ; suc )
open import Data.Product using ( _×_ ; _,′_ ) 
import Relation.Binary.HeterogeneousEquality.Quotients
open import Data.Product using (_,_)
open import Data.Product using (proj₁ ; proj₂ )

open import Relation.Binary.Core using (IsEquivalence ; _Respects_ ; _Respects₂_ )
open import Relation.Binary
open import Algebra.Structures
import Relation.Binary.EqReasoning as EqR
import Algebra.Properties.Group as GroupProperties
open import Algebra.Properties.Group using  (⁻¹-involutive)
open import Substructures using (IsNormalSubGroup; NormalSubGroup )
open import Util

module QuotientRelation where
--ab­1 ∈ H
QuotientRelation : {a ℓ : Level} (A : Set a) (H : Pred A ℓ) (_∙_ : Op₂ A) (_⁻¹ : Op₁ A) → Rel A ℓ
QuotientRelation A H _∙_ _⁻¹ a b = H (a ∙ (b ⁻¹))

-- A teraz Quotient Group
-- trzeba dodatkowe założenie że H jest relacją w normalnej podgrupie?
--Udowodnić że jak się podmieni ≈ na jakiś QuotientRelation to będzie dalej grupa!!
quotientGroupIsAGroup : ∀ {c b ℓ} (g : Group c ℓ) → let open Group g in (H : Pred Carrier b) →
  (IsNormalSubGroup _≈_ H _∙_ ε _⁻¹) →
  (IsGroup (QuotientRelation Carrier H _∙_ _⁻¹)  _∙_ ε _⁻¹ )
quotientGroupIsAGroup {c} {b} {ℓ} g@record { Carrier = Carrier ; _≈_ = _≈_ ; _∙_ = _∙_ ; ε = ε ; _⁻¹ = _⁻¹ ; isGroup = isGroup } H isNorm = let
  normalSubgroup : NormalSubGroup c b ℓ
  normalSubgroup = record
                     { Carrier = Carrier
                     ; IsInSubset = H
                     ; _≈_ = _≈_
                     ; _∙_ = _∙_
                     ; ε = ε
                     ; _⁻¹ = _⁻¹
                     ; isNormalSubGroup = isNorm
                     }
  quotientRel = (QuotientRelation Carrier H _∙_ _⁻¹)
  reflQ : Reflexive (λ a b₁ → H (a ∙ (b₁ ⁻¹)))
  reflQ = λ {x} → IsNormalSubGroup.≈_respect isNorm ((Group.sym g)  (proj₂ (Group.inverse g) x)) (IsNormalSubGroup.εInSubset isNorm)
  transQ : Transitive (λ z z₁ → H (z ∙ (z₁ ⁻¹)))
  transQ = λ {x} {y} {z} Rxy Ryz → let
    dd : H ((x ∙ (y ⁻¹)) ∙ (y ∙ (z ⁻¹)))
    dd = (IsNormalSubGroup.∙_isSubStructure isNorm) Rxy Ryz
    q1 : ((y ⁻¹) ∙ y) ≈ ε
    q1 = proj₁ (IsNormalSubGroup.inverse isNorm) y
    q2 : (x ∙ ((y ⁻¹) ∙ y)) ≈ x
    q2 = (IsNormalSubGroup.trans isNorm)  ((IsNormalSubGroup.∙-cong isNorm) ((IsNormalSubGroup.refl isNorm)  {x}) q1) (proj₂ (IsNormalSubGroup.identity isNorm) x)
    q2' : ((x ∙ (y ⁻¹)) ∙ y) ≈ (x ∙ ((y ⁻¹) ∙ y))
    q2' = ((IsNormalSubGroup.assoc isNorm) x (y ⁻¹) y )
    q3 : ((x ∙ (y ⁻¹)) ∙ y) ≈ x
    q3 = (IsNormalSubGroup.trans isNorm) q2' q2
    q5 :  (((x ∙ (y ⁻¹)) ∙ y) ∙ (z ⁻¹))  ≈ (x ∙ (z ⁻¹))
    q5 = (IsNormalSubGroup.∙-cong isNorm) q3 (IsNormalSubGroup.refl isNorm)
    q5' : ((x ∙ (y ⁻¹)) ∙ (y ∙ (z ⁻¹))) ≈ (((x ∙ (y ⁻¹)) ∙ y) ∙ (z ⁻¹))
    q5' = (IsNormalSubGroup.sym isNorm) ((IsNormalSubGroup.assoc isNorm) (x ∙ (y ⁻¹)) y (z ⁻¹)) 
    end : ((x ∙ (y ⁻¹)) ∙ (y ∙ (z ⁻¹))) ≈ ((x ∙ (z ⁻¹)))
    end = (IsNormalSubGroup.trans isNorm) q5' q5 
    in
    (IsNormalSubGroup.≈_respect isNorm) end dd
  symQ : Symmetric (λ a b₁ → H (a ∙ (b₁ ⁻¹)))
  symQ = λ {x} {y} Hxy →  let open IsNormalSubGroup isNorm in let
-- H x ∙ y⁻¹
-- H (y x-1) -1
-- preserves -1
    qq1 : ((x ∙ (y ⁻¹)) ⁻¹) ≈ (((y ⁻¹) ⁻¹) ∙ (x ⁻¹))
    qq1 = ∙⁻¹-distribution g x  (y ⁻¹)
    qq2 : ((y ⁻¹) ⁻¹) ≈ y
    qq2 = (⁻¹-involutive g y)
    end : ((x ∙ (y ⁻¹)) ⁻¹) ≈ (y ∙ (x ⁻¹))
    end = trans qq1 (∙-cong qq2 refl)
    in
    ≈_respect end (⁻¹_isSubStructure  Hxy) 
  isEquivalenceQ = record { refl = reflQ ; sym = symQ; trans = transQ }
-- JAK DO TEJ PORY ZUP{EŁNIE NIE WYKORZYSTAŁEM ZAŁOŻENIA ŻE PODGRUPA JEST NORMALNA!
  assocQ : Algebra.FunctionProperties.Associative quotientRel _∙_
  assocQ x y z = let open IsNormalSubGroup isNorm in let
    end : ε ≈ (((x ∙ y) ∙ z) ∙ ((x ∙ (y ∙ z)) ⁻¹))
    end = trans (sym  (inverseʳ (x ∙ (y ∙ z)))) (∙-cong (sym (assoc x y z)) refl)
    in
      ≈_respect end εInSubset
  ∙-congQ : Algebra.FunctionProperties.Congruent₂ quotientRel _∙_
  ∙-congQ = λ {a} {b} {c} {d} Hab⁻¹ Hcd⁻¹ → let open IsNormalSubGroup isNorm in let
{--
Zał : Hab⁻¹ Hcd⁻¹
Plan (pomijam łączność):
c ∙ d⁻¹
--isNorm a--  W KOŃCU SIĘ PRZYDAŁO XD
a ∙ c ∙ d⁻¹ ∙ a⁻¹
-- preserves ∙ 
a ∙ c ∙ d⁻¹ ∙ a⁻¹ ∙ a ∙ b⁻¹
a ∙ c ∙ d⁻¹ ∙ b⁻¹
a ∙ c ∙ (b ∙ d)⁻¹ 
--}
    start = H (((a ∙ (c ∙ (d ⁻¹))) ∙ (a ⁻¹)) ∙ (a ∙ (b ⁻¹)))
    start = ∙_isSubStructure (isNormal a _ Hcd⁻¹) Hab⁻¹
    qq2 : (((a ∙ (c ∙ (d ⁻¹))) ∙ (a ⁻¹)) ∙ (a ∙ (b ⁻¹))) ≈ ((((a ∙ (c ∙ (d ⁻¹))) ∙ (a ⁻¹)) ∙ a) ∙ (b ⁻¹))
    qq2 = sym (assoc ((a ∙ (c ∙ (d ⁻¹))) ∙ (a ⁻¹)) a _)
    qq2' : (((a ∙ (c ∙ (d ⁻¹))) ∙ (a ⁻¹)) ∙ a) ≈ ((a ∙ (c ∙ (d ⁻¹))) ∙ ((a ⁻¹) ∙ a))
    qq2' = assoc (a ∙ (c ∙ (d ⁻¹))) (a ⁻¹) a
    qq2'' : ((a ∙ (c ∙ (d ⁻¹))) ∙ ((a ⁻¹) ∙ a)) ≈ (a ∙ (c ∙ (d ⁻¹)))
    qq2'' = trans (∙-cong refl (inverseˡ a)) (identityʳ _)
    qq3 : (((a ∙ (c ∙ (d ⁻¹))) ∙ (a ⁻¹)) ∙ (a ∙ (b ⁻¹))) ≈ ((a ∙ (c ∙ (d ⁻¹))) ∙ (b ⁻¹))
    qq3 = trans qq2 (∙-cong (trans qq2' qq2'') (refl {(b ⁻¹)}))

    qq4 : ((a ∙ (c ∙ (d ⁻¹))) ∙ (b ⁻¹)) ≈ (((a ∙ c) ∙ (d ⁻¹)) ∙ (b ⁻¹))
    qq4 = ∙-cong (sym (assoc a c _)) refl
    qq4' : (((a ∙ c) ∙ (d ⁻¹)) ∙ (b ⁻¹)) ≈ (((a ∙ c) ∙ ((d ⁻¹) ∙ (b ⁻¹))))
    qq4' = assoc (a ∙ c) (d ⁻¹)  (b ⁻¹)

    end-1 : ((a ∙ (c ∙ (d ⁻¹))) ∙ (b ⁻¹)) ≈ ((a ∙ c) ∙ ((b ∙ d) ⁻¹))
    end-1 = trans qq4 (trans qq4' (∙-cong (refl {a ∙ c}) (sym (∙⁻¹-distribution g b d) )))
    end : (((a ∙ (c ∙ (d ⁻¹))) ∙ (a ⁻¹)) ∙ (a ∙ (b ⁻¹))) ≈ ((a ∙ c) ∙ ((b ∙ d) ⁻¹))
    end = trans qq3 end-1
    in
    ≈_respect end start
  identityLeftQ : Algebra.FunctionProperties.LeftIdentity quotientRel ε _∙_
  identityLeftQ = λ x → let open IsNormalSubGroup isNorm in 
    ≈_respect (trans (trans (sym (inverseʳ x)) (sym (identityˡ _))) (sym (assoc ε x (x ⁻¹)))) εInSubset
  identityRightQ : Algebra.FunctionProperties.RightIdentity quotientRel ε _∙_
  identityRightQ = λ x → let open IsNormalSubGroup isNorm in isNormal x ε εInSubset
  isSemigroupQ : IsSemigroup (λ a b₁ → H (a ∙ (b₁ ⁻¹))) _∙_
  isSemigroupQ = record { isMagma = record {isEquivalence = isEquivalenceQ ;  ∙-cong = ∙-congQ } ; assoc = assocQ }

  ⁻¹-congQ : Algebra.FunctionProperties.Congruent₁ quotientRel _⁻¹
  -- x H y -> x-1 H y-1
  ⁻¹-congQ = λ {x} {y} Hxy⁻¹ → let open IsNormalSubGroup isNorm in let
    --(⁻¹_isSubStructure  (symQ Hxy⁻¹))

    qe1 : y ≈((y ⁻¹) ⁻¹) 
    qe1 = sym (⁻¹-involutive g y)
    qe2 : (((y ⁻¹) ∙ (x ∙ (y ⁻¹))) ∙ ((y ⁻¹) ⁻¹)) ≈ (((y ⁻¹) ∙ (x ∙ (y ⁻¹))) ∙ y)
    qe2 = ∙-cong refl (sym qe1)
    qe3 : (((y ⁻¹) ∙ (x ∙ (y ⁻¹))) ∙ y) ≈ ((((y ⁻¹) ∙ x) ∙ (y ⁻¹)) ∙ y)
    qe3 = ∙-cong (sym (assoc (y ⁻¹) x (y ⁻¹))) (refl {y}) 
    qe4 : ((((y ⁻¹) ∙ x) ∙ (y ⁻¹)) ∙ y) ≈ (((y ⁻¹) ∙ x) ∙ ((y ⁻¹) ∙ y))
    qe4 =  (assoc ((y ⁻¹) ∙ x) (y ⁻¹) y)
    qe5 : (((y ⁻¹) ∙ x) ∙ ((y ⁻¹) ∙ y)) ≈ ((y ⁻¹) ∙ x)
    qe5 = trans (∙-cong refl (inverseˡ  y)) (identityʳ _)

    qq1 : H (((y ⁻¹) ∙ (x ∙ (y ⁻¹))) ∙ ((y ⁻¹) ⁻¹))
    qq1 =  (isNormal (y ⁻¹) _ Hxy⁻¹)
    qw1 : (((y ⁻¹) ∙ (x ∙ (y ⁻¹))) ∙ ((y ⁻¹) ⁻¹)) ≈ ((y ⁻¹) ∙ ((x ⁻¹) ⁻¹))
    qw1 = trans qe2 (trans qe3 (trans qe4 (trans qe5 (∙-cong (refl {y ⁻¹}) (sym (⁻¹-involutive g x)))))  )
    
    qw2a : H ((y ⁻¹) ∙ ((x ⁻¹) ⁻¹))
    qw2a = ≈_respect qw1 qq1

    in
      symQ qw2a
  isMonoidQ : IsMonoid quotientRel _∙_ ε
  isMonoidQ = record { isSemigroup = isSemigroupQ ; identity = identityLeftQ , identityRightQ }
  leftInverseQ : Algebra.FunctionProperties.LeftInverse quotientRel ε _⁻¹ _∙_
  leftInverseQ = λ x → let open IsNormalSubGroup isNorm in
    ≈_respect (trans (sym (inverseʳ ε)) (∙-cong (sym (inverseˡ x)) (refl {ε ⁻¹}))) εInSubset
  rightInverseQ : Algebra.FunctionProperties.RightInverse quotientRel ε _⁻¹ _∙_
  rightInverseQ = λ x → let open IsNormalSubGroup isNorm in
    ≈_respect (trans (sym (inverseʳ ε)) (∙-cong (sym (inverseʳ x)) (refl {ε ⁻¹}))) εInSubset
  in
  record {isMonoid = isMonoidQ; ⁻¹-cong = ⁻¹-congQ ; inverse = leftInverseQ , rightInverseQ}
